$\forall$$A$, $B$:Type.
\\[0ex]AtomFree(Type;$B$) $\Rightarrow$ AtomFree(Type;$A$) $\Rightarrow$ $A$ $\subseteq\rho$ $B$ $\Rightarrow$ ($\forall$$x$:$A$, $a$:Atom1. $x$:$B$$>>$$a$ $\Rightarrow$ $x$:$A$$>>$$a$)